es:event_system{i:l}, as,bs:(es-E(es) List).
loc-ordered(es; as)
 loc-ordered(es; bs)
 ((as = bs)  (e:es-E(es). (e  as)  (e  bs))) 

latex

Definitions	t  T, x:A. B(x), void, x:AB(x), P  Q, False, A, x.A(x), event_system{i:l}, type List, loc-ordered(es; L), s = t, (x  l), P  Q, es-locl(es; e; e'), x,y. t(x;y), es-E(es), trans(T; x,y.E(x;y)), x:A  B(x), P  Q
Lemmas	es-axioms, event system wf, l-ordered-equality, es-locl-antireflexive, es-locl wf, es-E wf